The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳30 CdtProblem
    ↳31 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳32 CdtProblem
↳33 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳34 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

g(x, x) → g(a, b)
g(c, g(c, x)) → g(e, g(d, x))
g(d, g(d, x)) → g(c, g(e, x))
g(e, g(e, x)) → g(d, g(c, x))
f(g(x, y)) → g(y, g(f(f(x)), a))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(z0, z0) → c1(G(a, b))
G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
S tuples:

G(z0, z0) → c1(G(a, b))
G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c1, c2, c3, c4, c5

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

G(z0, z0) → c1(G(a, b))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
S tuples:

G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c2, c3, c4, c5

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0)) by

G(c, g(c, d)) → c2(G(e, g(a, b)), G(d, d))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(c, g(c, x0)) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, d)) → c2(G(e, g(a, b)), G(d, d))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(c, g(c, x0)) → c2
S tuples:

G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, d)) → c2(G(e, g(a, b)), G(d, d))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(c, g(c, x0)) → c2
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c3, c4, c5, c2, c2

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(c, g(c, x0)) → c2
G(c, g(c, d)) → c2(G(e, g(a, b)), G(d, d))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
S tuples:

G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c3, c4, c5, c2

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0)) by

G(d, g(d, e)) → c3(G(c, g(a, b)), G(e, e))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(d, g(d, x0)) → c3

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, e)) → c3(G(c, g(a, b)), G(e, e))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(d, g(d, x0)) → c3
S tuples:

G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, e)) → c3(G(c, g(a, b)), G(e, e))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(d, g(d, x0)) → c3
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c2, c3, c3

(11) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(d, g(d, x0)) → c3
G(d, g(d, e)) → c3(G(c, g(a, b)), G(e, e))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
S tuples:

G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c2, c3

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0)) by

G(e, g(e, c)) → c4(G(d, g(a, b)), G(c, c))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
G(e, g(e, x0)) → c4

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, c)) → c4(G(d, g(a, b)), G(c, c))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
G(e, g(e, x0)) → c4
S tuples:

F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, c)) → c4(G(d, g(a, b)), G(c, c))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
G(e, g(e, x0)) → c4
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

F, G

Compound Symbols:

c5, c2, c3, c4, c4

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(e, g(e, c)) → c4(G(d, g(a, b)), G(c, c))
G(e, g(e, x0)) → c4

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
S tuples:

F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0))
G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

F, G

Compound Symbols:

c5, c2, c3, c4

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(g(z0, z1)) → c5(G(z1, g(f(f(z0)), a)), G(f(f(z0)), a), F(f(z0)), F(z0)) by

F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5
S tuples:

G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
F(g(x0, x1)) → c5
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c2, c3, c4, c5, c5

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(g(x0, x1)) → c5

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
S tuples:

G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0)))
G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c2, c3, c4, c5

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(c, g(c, g(d, z0))) → c2(G(e, g(c, g(e, z0))), G(d, g(d, z0))) by

G(c, g(c, g(d, e))) → c2(G(e, g(c, g(a, b))), G(d, g(d, e)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(c, g(c, g(d, x0))) → c2

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, e))) → c2(G(e, g(c, g(a, b))), G(d, g(d, e)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(c, g(c, g(d, x0))) → c2
S tuples:

G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, e))) → c2(G(e, g(c, g(a, b))), G(d, g(d, e)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(c, g(c, g(d, x0))) → c2
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c3, c4, c5, c2, c2

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(c, g(c, g(d, e))) → c2(G(e, g(c, g(a, b))), G(d, g(d, e)))
G(c, g(c, g(d, x0))) → c2

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
S tuples:

G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0)))
G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c3, c4, c5, c2

(25) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(d, g(d, g(e, z0))) → c3(G(c, g(d, g(c, z0))), G(e, g(e, z0))) by

G(d, g(d, g(e, c))) → c3(G(c, g(d, g(a, b))), G(e, g(e, c)))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(d, g(d, g(e, x0))) → c3

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, c))) → c3(G(c, g(d, g(a, b))), G(e, g(e, c)))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(d, g(d, g(e, x0))) → c3
S tuples:

G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, c))) → c3(G(c, g(d, g(a, b))), G(e, g(e, c)))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(d, g(d, g(e, x0))) → c3
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c2, c3, c3

(27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(d, g(d, g(e, x0))) → c3
G(d, g(d, g(e, c))) → c3(G(c, g(d, g(a, b))), G(e, g(e, c)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
S tuples:

G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0)))
F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c2, c3

(29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(e, g(e, g(c, z0))) → c4(G(d, g(e, g(d, z0))), G(c, g(c, z0))) by

G(e, g(e, g(c, d))) → c4(G(d, g(e, g(a, b))), G(c, g(c, d)))
G(e, g(e, g(c, g(d, z0)))) → c4(G(d, g(e, g(c, g(e, z0)))), G(c, g(c, g(d, z0))))
G(e, g(e, g(c, x0))) → c4

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(e, g(e, g(c, d))) → c4(G(d, g(e, g(a, b))), G(c, g(c, d)))
G(e, g(e, g(c, g(d, z0)))) → c4(G(d, g(e, g(c, g(e, z0)))), G(c, g(c, g(d, z0))))
G(e, g(e, g(c, x0))) → c4
S tuples:

F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(e, g(e, g(c, d))) → c4(G(d, g(e, g(a, b))), G(c, g(c, d)))
G(e, g(e, g(c, g(d, z0)))) → c4(G(d, g(e, g(c, g(e, z0)))), G(c, g(c, g(d, z0))))
G(e, g(e, g(c, x0))) → c4
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

F, G

Compound Symbols:

c5, c2, c3, c4, c4

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

G(e, g(e, g(c, d))) → c4(G(d, g(e, g(a, b))), G(c, g(c, d)))
G(e, g(e, g(c, x0))) → c4

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(z0, z0) → g(a, b)
g(c, g(c, z0)) → g(e, g(d, z0))
g(d, g(d, z0)) → g(c, g(e, z0))
g(e, g(e, z0)) → g(d, g(c, z0))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:

F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(e, g(e, g(c, g(d, z0)))) → c4(G(d, g(e, g(c, g(e, z0)))), G(c, g(c, g(d, z0))))
S tuples:

F(g(g(z0, z1), x1)) → c5(G(x1, g(f(g(z1, g(f(f(z0)), a))), a)), G(f(f(g(z0, z1))), a), F(f(g(z0, z1))), F(g(z0, z1)))
G(c, g(c, g(d, g(e, z0)))) → c2(G(e, g(c, g(d, g(c, z0)))), G(d, g(d, g(e, z0))))
G(d, g(d, g(e, g(c, z0)))) → c3(G(c, g(d, g(e, g(d, z0)))), G(e, g(e, g(c, z0))))
G(e, g(e, g(c, g(d, z0)))) → c4(G(d, g(e, g(c, g(e, z0)))), G(c, g(c, g(d, z0))))
K tuples:none
Defined Rule Symbols:

g, f

Defined Pair Symbols:

F, G

Compound Symbols:

c5, c2, c3, c4

(33) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
c0() → 0
e0() → 0
d0() → 0
g0(0, 0) → 1
f0(0) → 2
a1() → 3
b1() → 4
g1(3, 4) → 1
a1() → 0
b1() → 0
a1() → 5
b1() → 6
g0(5, 0) → 1
g0(0, 5) → 1
g0(6, 0) → 1
g0(0, 6) → 1
g0(5, 5) → 1
g0(5, 6) → 1
g0(6, 5) → 1
g0(6, 6) → 1
f0(5) → 2
f0(6) → 2
g1(5, 4) → 1
g1(3, 6) → 1
g1(5, 6) → 1

(34) BOUNDS(O(1), O(n^1))